YES 1.464
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule Main
| ((readInt :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) |
module Main where
Lambda Reductions:
The following Lambda expression
\nd→n * radix + d
is transformed to
readInt0 | radix n d | = n * radix + d |
The following Lambda expression
\vu77→
case | vu77 of |
| (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
is transformed to
readInt1 | radix digToInt vu77 | =
case | vu77 of | | (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
|
The following Lambda expression
\vu68→
case | vu68 of |
| (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
is transformed to
nonnull0 | vu68 | =
case | vu68 of | | (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
|
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule Main
| ((readInt :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) |
module Main where
Case Reductions:
The following Case expression
case | vu77 of |
| (ds,r) | → (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
| _ | → [] |
is transformed to
readInt10 | radix digToInt (ds,r) | = (foldl1 (readInt0 radix) (map (fromIntegral . digToInt) ds),r) : [] |
readInt10 | radix digToInt _ | = [] |
The following Case expression
case | vu68 of |
| (cs@(_ : _),t) | → (cs,t) : [] |
| _ | → [] |
is transformed to
nonnull00 | (cs@(_ : _),t) | = (cs,t) : [] |
nonnull00 | _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
mainModule Main
| ((readInt :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
cs@(vy : vz)
is replaced by the following term
vy : vz
The bind variable of the following binding Pattern
xs@(ww : wx)
is replaced by the following term
ww : wx
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((readInt :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
span | p [] | = ([],[]) |
span | p (ww : wx) | |
is transformed to
span | p [] | = span3 p [] |
span | p (ww : wx) | = span2 p (ww : wx) |
span2 | p (ww : wx) | =
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
|
span3 | p [] | = ([],[]) |
span3 | xx xy | = span2 xx xy |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule Main
| ((readInt :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) |
module Main where
Let/Where Reductions:
The bindings of the following Let/Where expression
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
are unpacked to the following functions on top level
span2Ys | xz yu | = span2Ys0 xz yu (span2Vu43 xz yu) |
span2Span0 | xz yu p ww wx True | = ([],ww : wx) |
span2Zs | xz yu | = span2Zs0 xz yu (span2Vu43 xz yu) |
span2Vu43 | xz yu | = span xz yu |
span2Ys0 | xz yu (ys,wy) | = ys |
span2Zs0 | xz yu (wz,zs) | = zs |
span2Span1 | xz yu p ww wx True | = (ww : span2Ys xz yu,span2Zs xz yu) |
span2Span1 | xz yu p ww wx False | = span2Span0 xz yu p ww wx otherwise |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
mainModule Main
| (readInt :: Int -> (Char -> Bool) -> (Char -> Int) -> [Char] -> [(Int,[Char])]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs(yv4, :(yv610, yv611)) → new_span2Zs0(yv4, yv610, yv611)
new_span2Zs0(yv4, yv610, yv611) → new_span2Zs(yv4, yv611)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs0(yv4, yv610, yv611) → new_span2Zs(yv4, yv611)
The graph contains the following edges 1 >= 1, 3 >= 2
- new_span2Zs(yv4, :(yv610, yv611)) → new_span2Zs0(yv4, yv610, yv611)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMinusNat(Succ(yv180), Succ(yv1500)) → new_primMinusNat(yv180, yv1500)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMinusNat(Succ(yv180), Succ(yv1500)) → new_primMinusNat(yv180, yv1500)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(yv190), Succ(yv1500)) → new_primPlusNat(yv190, yv1500)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(yv190), Succ(yv1500)) → new_primPlusNat(yv190, yv1500)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(yv1400), Succ(yv300)) → new_primMulNat(yv1400, Succ(yv300))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(yv1400), Succ(yv300)) → new_primMulNat(yv1400, Succ(yv300))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldl(yv3, yv14, yv5, yv4, yv610, yv611, yv12) → new_foldl0(yv3, yv14, new_pt(yv5, yv610), yv5, yv4, yv611)
new_foldl1(yv3, yv14, yv15, yv5, yv4, yv6110, yv6111) → new_foldl(yv3, new_readInt0(yv3, yv14, yv15), yv5, yv4, yv6110, yv6111, new_span2Zs1(yv4, yv6111))
new_foldl0(yv3, yv14, yv15, yv5, yv4, :(yv6110, yv6111)) → new_foldl1(yv3, yv14, yv15, yv5, yv4, yv6110, yv6111)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_readInt0(Neg(yv30), Pos(yv140), yv15) → new_primPlusInt(yv140, yv30, yv15)
new_readInt0(Pos(yv30), Neg(yv140), yv15) → new_primPlusInt(yv140, yv30, yv15)
new_primPlusInt(yv140, yv30, Neg(yv150)) → Neg(new_primPlusNat0(new_primMulNat0(yv140, yv30), yv150))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusInt(yv140, yv30, Pos(yv150)) → new_primMinusNat0(yv150, new_primMulNat0(yv140, yv30))
new_readInt0(Neg(yv30), Neg(yv140), yv15) → new_primPlusInt0(yv140, yv30, yv15)
new_primPlusInt0(yv140, yv30, Pos(yv150)) → Pos(new_primPlusNat0(new_primMulNat0(yv140, yv30), yv150))
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_primMinusNat0(Succ(yv180), Zero) → Pos(Succ(yv180))
new_primPlusInt0(yv140, yv30, Neg(yv150)) → new_primMinusNat0(new_primMulNat0(yv140, yv30), yv150)
new_readInt0(Pos(yv30), Pos(yv140), yv15) → new_primPlusInt0(yv140, yv30, yv15)
new_primMulNat0(Zero, Succ(yv300)) → Zero
new_primMulNat0(Succ(yv1400), Zero) → Zero
new_primMulNat0(Succ(yv1400), Succ(yv300)) → new_primPlusNat0(new_primMulNat0(yv1400, Succ(yv300)), Succ(yv300))
new_primPlusNat0(Zero, Succ(yv1500)) → Succ(yv1500)
new_primPlusNat0(Succ(yv190), Zero) → Succ(yv190)
new_primMinusNat0(Zero, Succ(yv1500)) → Neg(Succ(yv1500))
new_primPlusNat0(Succ(yv190), Succ(yv1500)) → Succ(Succ(new_primPlusNat0(yv190, yv1500)))
new_primMinusNat0(Succ(yv180), Succ(yv1500)) → new_primMinusNat0(yv180, yv1500)
The set Q consists of the following terms:
new_primPlusNat0(Zero, Succ(x0))
new_primPlusInt0(x0, x1, Neg(x2))
new_primPlusInt(x0, x1, Pos(x2))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusInt(x0, x1, Neg(x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_readInt0(Pos(x0), Neg(x1), x2)
new_readInt0(Neg(x0), Pos(x1), x2)
new_primMulNat0(Zero, Zero)
new_primPlusInt0(x0, x1, Pos(x2))
new_readInt0(Pos(x0), Pos(x1), x2)
new_primMinusNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primMinusNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_primMulNat0(Succ(x0), Zero)
new_readInt0(Neg(x0), Neg(x1), x2)
new_primMinusNat0(Zero, Zero)
new_primMinusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldl0(yv3, yv14, yv15, yv5, yv4, :(yv6110, yv6111)) → new_foldl1(yv3, yv14, yv15, yv5, yv4, yv6110, yv6111)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 6 > 7
- new_foldl1(yv3, yv14, yv15, yv5, yv4, yv6110, yv6111) → new_foldl(yv3, new_readInt0(yv3, yv14, yv15), yv5, yv4, yv6110, yv6111, new_span2Zs1(yv4, yv6111))
The graph contains the following edges 1 >= 1, 4 >= 3, 5 >= 4, 6 >= 5, 7 >= 6
- new_foldl(yv3, yv14, yv5, yv4, yv610, yv611, yv12) → new_foldl0(yv3, yv14, new_pt(yv5, yv610), yv5, yv4, yv611)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5, 6 >= 6